/**
 * @file solver.h
 * @brief Algorithme de resolution
 * @author Radim BADSI, Kévin CHAPON, Fanny FERLET
 */
#ifndef SOLVER_H
#define SOLVER_H

#include "matrice.h"

/**
 * Structure de passage de paramètres à la fonction tester.
 * Il est nécessaire de passer par une structure car un thread
 * ne peut prendre qu'un seul paramètre.
 */
typedef struct {
	t_matrice* matrice;				/*!< Matrice.*/
	t_clause* tab_clauses;			/*!< Tableau de clauses. */
	t_litteral* tab_variables;		/*!< Tableau des variables. */
	t_matrice* nouv_matrice;		/*!< Nouvelle matrice. */
	t_clause* nouv_tab_clauses;		/*!< Nouveau tableau de clauses. */
	t_litteral* nouv_tab_variables;	/*!< Nouveau tableau de variables. */
	int niv;						/*!< Niveau de résolution. */
	int variable_choisie;			/*!< Numéro de variable. */
	int thread;						/*!< Thread. */
} tester_param_t;

/**
 * Initialise le support du multithreading.
 */
void init_threading();

/**
 * Affecte une valeur VRAI ou FAUX à une variable.
 * @param matrice Matrice
 * @param tab_clauses tableau de clauses
 * @param tab_variables tableau de variables
 * @param num_var_courante numéro et signe de la variable à affecter
 * @return code erreur -1 sinon 1.
 */
int affecter (t_matrice* matrice,
			 t_clause* tab_clauses,
			 t_litteral* tab_variables,
			 int num_var_courante);

/**
 * Recherche et traitement des litteraux propres.
 * Simplifie la matrice tant qu'il y existe des litteraux propres.
 * @param matrice Matrice
 * @param tab_clauses tableau de clauses
 * @param tab_variables tableau de variables  
 * @return 1 sinon -1 en cas d'erreur.
 */
int traiter_litteraux_propres (t_matrice* matrice,
				t_clause* tab_clauses,
				t_litteral* tab_variables
				);
				
/**
 * Recherche et traitement des clauses unitaires.
 * Simplifie la matrice tant qu'il y existe des clauses unitaires.
 * @param matrice Matrice
 * @param tab_clauses tableau de clauses
 * @param tab_variables tableau de variables  
 * @return 1 sinon -1 en cas d'erreur.
 */
int traiter_clauses_unitaires (t_matrice* matrice,
			    t_clause* tab_clauses,
			    t_litteral* tab_variables);

/**
 * Recherche le numéro d'une variable a affecter.
 * Variable qui est dans le plus de clauses à satisfaire.
 * @param tab_variables tableau des variables
 * @return numéro de la variable, si aucune variable possible 0.
 */
int choisir_var (t_litteral* tab_variables);

/**
 * Permet la résolution des clauses.
 * @param matrice Matrice
 * @param tab_clauses tableau de clauses
 * @param tab_variables tableau de variables
 * @param niv niveau de retour en arrière
 * @return 1 si une solution a été trouvée.
 */
int resoudre (t_matrice* matrice,
			  t_clause* tab_clauses,
			  t_litteral* tab_variables,
			    int niv);

/**
 * Décrémente le compteur des occurrences.
 * @param tab_variables tableau de variables
 * @param num_var numéro de la variable
 */
void decr_compteur_occ (t_litteral* tab_variables, int num_var);

/**
 * Met a jour les compteurs d'occurrences des variables d'une clause.
 * @param matrice Matrice
 * @param tab_clauses tableau de clauses
 * @param tab_variables tableau de variables
 * @param num_clause numéro de la clause
 */
void mettre_a_jour_compteurs_occ (t_matrice* matrice,
			   t_clause* tab_clauses,
			   t_litteral* tab_variables,
			   int num_clause);

/**
 * Simplifie la matrice.
 * Satisfait ou raccourcie des clauses suivant l'affectation d'une variable.
 * @param matrice Matrice
 * @param tab_clauses tableau de clauses
 * @param tab_variables tableau de variables
 * @param num_var_courante numéro de la variable
 * @return -1 si une clause est falsifiée sinon 0.
 */	
int simplifier (t_matrice* matrice,
			   t_clause* tab_clauses,
			   t_litteral* tab_variables,
			   int num_var_courante);
/**
 * Affectations et test de satisfiabilité.
 * @param tester_param ensemble des variables de la matrice
 * @return 1 si toutes les clauses sont satisfaites sinon résultat de resoudre.
 */
int tester (tester_param_t *tester_param);

#endif